Inference at * 
Iof proof for Lemma can-apply-p-co-filter:


  T:Type, P:(T), f:(x:T. Dec(P(x))), x:T. (can-apply(p-co-filter(f);x))  (P(x)) 

latex

 by ((((UnivCD) 
CollapseTHENA (Auto))) 
CollapseTHEN (RepUR ``can-apply p-co-filter`` ( 0)))
Co 

latex

Co1: 

Co1: 1. T : Type
Co1: 2. P : T
Co1: 3. f : x:T. Dec(P(x))
Co1: 4. x : T
Co1:   (isl(case f(x) of inl(p) => inr p  | inr(p) => inl x ))  (P(x))
Co.

Definitions	Dec(P), x:A. B(x), x(s), f(a), x:AB(x), , t  T, Type, p-co-filter(f), can-apply(f;x), b
Lemmas	decidable wf